Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		p(0)	→ 0
2:		p(s(x))	→ x
3:		plus(x,0)	→ x
4:		plus(0,y)	→ y
5:		plus(s(x),y)	→ s(plus(x,y))
6:		plus(s(x),y)	→ s(plus(p(s(x)),y))
7:		plus(x,s(y))	→ s(plus(x,p(s(y))))
8:		times(0,y)	→ 0
9:		times(s(0),y)	→ y
10:		times(s(x),y)	→ plus(y,times(x,y))
11:		div(0,y)	→ 0
12:		div(x,y)	→ quot(x,y,y)
13:		quot(0,s(y),z)	→ 0
14:		quot(s(x),s(y),z)	→ quot(x,y,z)
15:		quot(x,0,s(z))	→ s(div(x,s(z)))
16:		div(div(x,y),z)	→ div(x,times(y,z))
17:		eq(0,0)	→ true
18:		eq(s(x),0)	→ false
19:		eq(0,s(y))	→ false
20:		eq(s(x),s(y))	→ eq(x,y)
21:		divides(y,x)	→ eq(x,times(div(x,y),y))
22:		prime(s(s(x)))	→ pr(s(s(x)),s(x))
23:		pr(x,s(0))	→ true
24:		pr(x,s(s(y)))	→ if(divides(s(s(y)),x),x,s(y))
25:		if(true,x,y)	→ false
26:		if(false,x,y)	→ pr(x,y)

There are 20 dependency pairs:


27:		PLUS(s(x),y)	→ PLUS(x,y)
28:		PLUS(s(x),y)	→ PLUS(p(s(x)),y)
29:		PLUS(s(x),y)	→ P(s(x))
30:		PLUS(x,s(y))	→ PLUS(x,p(s(y)))
31:		PLUS(x,s(y))	→ P(s(y))
32:		TIMES(s(x),y)	→ PLUS(y,times(x,y))
33:		TIMES(s(x),y)	→ TIMES(x,y)
34:		DIV(x,y)	→ QUOT(x,y,y)
35:		QUOT(s(x),s(y),z)	→ QUOT(x,y,z)
36:		QUOT(x,0,s(z))	→ DIV(x,s(z))
37:		DIV(div(x,y),z)	→ DIV(x,times(y,z))
38:		DIV(div(x,y),z)	→ TIMES(y,z)
39:		EQ(s(x),s(y))	→ EQ(x,y)
40:		DIVIDES(y,x)	→ EQ(x,times(div(x,y),y))
41:		DIVIDES(y,x)	→ TIMES(div(x,y),y)
42:		DIVIDES(y,x)	→ DIV(x,y)
43:		PRIME(s(s(x)))	→ PR(s(s(x)),s(x))
44:		PR(x,s(s(y)))	→ IF(divides(s(s(y)),x),x,s(y))
45:		PR(x,s(s(y)))	→ DIVIDES(s(s(y)),x)
46:		IF(false,x,y)	→ PR(x,y)

The approximated dependency graph contains 5 SCCs: {39}, {27,28,30}, {33}, {34-37} and {44,46}.

Consider the SCC {39}. There are no usable rules. By taking the AF π with π(EQ) = 1 together with the lexicographic path order with empty precedence, rule 39 is strictly decreasing.

Consider the SCC {27,28,30}. The usable rules are {1,2}. By taking the AF π with π(p) = π(PLUS) = 1 together with the lexicographic path order with empty precedence, the rules in {1,28,30} are weakly decreasing and the rules in {2,27} are strictly decreasing. There is one new SCC.
- Consider the SCC {28,30}. The constraints could not be solved.

Consider the SCC {33}. There are no usable rules. By taking the AF π with π(TIMES) = 1 together with the lexicographic path order with empty precedence, rule 33 is strictly decreasing.

Consider the SCC {34-37}. The usable rules are {1-10}. The constraints could not be solved.

Consider the SCC {44,46}. The usable rules are {1-21}. The constraints could not be solved.

Tyrolean Termination Tool (2.08 seconds) --- May 3, 2006